thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1
THRICE(s(x1)) → P(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))
SIXTIMES(s(x1)) → P(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))
HALF(s(s(x1))) → P(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
HALF(s(x1)) → P(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))
HALF(0(x1)) → 01(p(s(s(s(s(x1))))))
SIXTIMES(s(x1)) → P(p(s(s(s(x1)))))
THRICE(s(x1)) → HALF(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))
THRICE(s(x1)) → P(s(s(x1)))
THRICE(s(x1)) → P(s(p(p(s(s(x1))))))
THRICE(s(x1)) → P(p(s(s(x1))))
THRICE(0(x1)) → P(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
HALF(s(x1)) → P(s(x1))
HALF(s(s(x1))) → P(p(s(s(half(p(p(s(s(p(s(x1)))))))))))
SIXTIMES(0(x1)) → P(s(p(s(x1))))
HALF(s(s(x1))) → P(p(s(s(p(s(x1))))))
SIXTIMES(0(x1)) → 01(s(s(s(s(s(p(s(p(s(x1))))))))))
SIXTIMES(s(x1)) → P(s(p(p(p(s(s(s(x1))))))))
SIXTIMES(s(x1)) → P(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))
HALF(0(x1)) → P(s(0(p(s(s(s(s(x1))))))))
HALF(s(x1)) → P(p(s(s(half(p(p(s(s(p(s(x1)))))))))))
P(p(s(x1))) → P(x1)
THRICE(s(x1)) → P(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))
THRICE(0(x1)) → P(s(p(s(x1))))
THRICE(s(x1)) → SIXTIMES(p(s(p(p(s(s(x1)))))))
THRICE(s(x1)) → P(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))))))
SIXTIMES(0(x1)) → P(s(x1))
HALF(s(x1)) → P(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))
HALF(0(x1)) → P(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
THRICE(0(x1)) → P(p(s(s(s(0(p(s(p(s(x1))))))))))
HALF(0(x1)) → P(s(s(p(s(0(p(s(s(s(s(x1)))))))))))
THRICE(s(x1)) → P(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
HALF(s(s(x1))) → P(s(s(p(s(x1)))))
THRICE(0(x1)) → P(p(p(s(s(s(0(p(s(p(s(x1)))))))))))
HALF(s(x1)) → P(p(s(s(p(s(x1))))))
SIXTIMES(s(x1)) → P(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
HALF(s(x1)) → P(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
HALF(s(s(x1))) → HALF(p(p(s(s(p(s(x1)))))))
SIXTIMES(s(x1)) → P(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))
THRICE(0(x1)) → P(s(s(s(0(p(s(p(s(x1)))))))))
SIXTIMES(0(x1)) → P(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
P(0(x1)) → 01(s(s(s(s(x1)))))
SIXTIMES(0(x1)) → P(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))
SIXTIMES(s(x1)) → P(s(s(s(x1))))
SIXTIMES(s(x1)) → P(p(p(s(s(s(x1))))))
HALF(s(x1)) → HALF(p(p(s(s(p(s(x1)))))))
HALF(s(x1)) → P(s(s(half(p(p(s(s(p(s(x1))))))))))
HALF(s(x1)) → P(s(s(p(s(x1)))))
HALF(0(x1)) → P(s(s(s(s(x1)))))
THRICE(0(x1)) → 01(p(s(p(s(x1)))))
HALF(s(s(x1))) → P(s(x1))
SIXTIMES(s(x1)) → SIXTIMES(p(s(p(p(p(s(s(s(x1)))))))))
HALF(s(s(x1))) → P(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))
THRICE(s(x1)) → P(s(sixtimes(p(s(p(p(s(s(x1)))))))))
THRICE(0(x1)) → P(s(x1))
SIXTIMES(s(x1)) → P(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))
HALF(s(s(x1))) → P(s(s(half(p(p(s(s(p(s(x1))))))))))
thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
THRICE(s(x1)) → P(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))
SIXTIMES(s(x1)) → P(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))
HALF(s(s(x1))) → P(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
HALF(s(x1)) → P(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))
HALF(0(x1)) → 01(p(s(s(s(s(x1))))))
SIXTIMES(s(x1)) → P(p(s(s(s(x1)))))
THRICE(s(x1)) → HALF(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))
THRICE(s(x1)) → P(s(s(x1)))
THRICE(s(x1)) → P(s(p(p(s(s(x1))))))
THRICE(s(x1)) → P(p(s(s(x1))))
THRICE(0(x1)) → P(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
HALF(s(x1)) → P(s(x1))
HALF(s(s(x1))) → P(p(s(s(half(p(p(s(s(p(s(x1)))))))))))
SIXTIMES(0(x1)) → P(s(p(s(x1))))
HALF(s(s(x1))) → P(p(s(s(p(s(x1))))))
SIXTIMES(0(x1)) → 01(s(s(s(s(s(p(s(p(s(x1))))))))))
SIXTIMES(s(x1)) → P(s(p(p(p(s(s(s(x1))))))))
SIXTIMES(s(x1)) → P(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))
HALF(0(x1)) → P(s(0(p(s(s(s(s(x1))))))))
HALF(s(x1)) → P(p(s(s(half(p(p(s(s(p(s(x1)))))))))))
P(p(s(x1))) → P(x1)
THRICE(s(x1)) → P(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))
THRICE(0(x1)) → P(s(p(s(x1))))
THRICE(s(x1)) → SIXTIMES(p(s(p(p(s(s(x1)))))))
THRICE(s(x1)) → P(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))))))
SIXTIMES(0(x1)) → P(s(x1))
HALF(s(x1)) → P(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))
HALF(0(x1)) → P(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
THRICE(0(x1)) → P(p(s(s(s(0(p(s(p(s(x1))))))))))
HALF(0(x1)) → P(s(s(p(s(0(p(s(s(s(s(x1)))))))))))
THRICE(s(x1)) → P(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
HALF(s(s(x1))) → P(s(s(p(s(x1)))))
THRICE(0(x1)) → P(p(p(s(s(s(0(p(s(p(s(x1)))))))))))
HALF(s(x1)) → P(p(s(s(p(s(x1))))))
SIXTIMES(s(x1)) → P(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
HALF(s(x1)) → P(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
HALF(s(s(x1))) → HALF(p(p(s(s(p(s(x1)))))))
SIXTIMES(s(x1)) → P(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))
THRICE(0(x1)) → P(s(s(s(0(p(s(p(s(x1)))))))))
SIXTIMES(0(x1)) → P(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
P(0(x1)) → 01(s(s(s(s(x1)))))
SIXTIMES(0(x1)) → P(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))
SIXTIMES(s(x1)) → P(s(s(s(x1))))
SIXTIMES(s(x1)) → P(p(p(s(s(s(x1))))))
HALF(s(x1)) → HALF(p(p(s(s(p(s(x1)))))))
HALF(s(x1)) → P(s(s(half(p(p(s(s(p(s(x1))))))))))
HALF(s(x1)) → P(s(s(p(s(x1)))))
HALF(0(x1)) → P(s(s(s(s(x1)))))
THRICE(0(x1)) → 01(p(s(p(s(x1)))))
HALF(s(s(x1))) → P(s(x1))
SIXTIMES(s(x1)) → SIXTIMES(p(s(p(p(p(s(s(s(x1)))))))))
HALF(s(s(x1))) → P(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))
THRICE(s(x1)) → P(s(sixtimes(p(s(p(p(s(s(x1)))))))))
THRICE(0(x1)) → P(s(x1))
SIXTIMES(s(x1)) → P(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))
HALF(s(s(x1))) → P(s(s(half(p(p(s(s(p(s(x1))))))))))
thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
P(p(s(x1))) → P(x1)
thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(p(s(x1))) → P(x1)
The value of delta used in the strict ordering is 2.
POL(P(x1)) = (2)x_1
POL(p(x1)) = 1 + x_1
POL(s(x1)) = x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
SIXTIMES(s(x1)) → SIXTIMES(p(s(p(p(p(s(s(s(x1)))))))))
thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
HALF(s(s(x1))) → HALF(p(p(s(s(p(s(x1)))))))
HALF(s(x1)) → HALF(p(p(s(s(p(s(x1)))))))
thrice(0(x1)) → p(s(p(p(p(s(s(s(0(p(s(p(s(x1)))))))))))))
thrice(s(x1)) → p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1))))))))))))))))))
half(0(x1)) → p(p(s(s(p(s(0(p(s(s(s(s(x1))))))))))))
half(s(x1)) → p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))))
half(s(s(x1))) → p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))
sixtimes(0(x1)) → p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1))))))))))))))
sixtimes(s(x1)) → p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(x1)))))
0(x1) → x1